M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id. ma-ef-const(M;k;x;s;v)   

latex

Definitions	t  T, IdDeq, Id, x:A. B(x), Type, Void, f(x)?z, Top, x.A(x), x. t(x), x:AB(x), S  T, Valtype(da;k), Knd, State(ds), KindDeq, <a, b>, t.2, x:A  B(x), , t.1, a:A fp B(a), product-deq(A;B;a;b), P  Q, f(x), f(a), suptype(S; T), constant_function(f;A;B), x  dom(f), b, , z != f(x)  P(a;z), M.ds(x), ma-ef-const(M;k;x;s;v), M.da(a), M.state, MsgA
Lemmas	msga wf, assert wf, fpf-dom wf, constant function wf, fpf-ap wf, product-deq wf, fpf-trivial-subtype-top, ma-valtype wf, pi1 wf, rationals wf, pi2 wf, Kind-deq wf, top wf, ma-state wf, Knd wf, fpf-cap wf, fpf-cap-void-subtype, Id wf, id-deq wf